home *** CD-ROM | disk | FTP | other *** search
/ Celestin Apprentice 4 / Apprentice-Release4.iso / Languages / Caml Light 0.7 / examples / demonstr / prop.ml < prev    next >
Encoding:
Text File  |  1995-06-01  |  1.3 KB  |  34 lines  |  [TEXT/MPS ]
  1. let rec évalue_dans liaisons = function
  2.     Vrai -> true
  3.   | Faux -> false
  4.   | Non p -> not (évalue_dans liaisons p)
  5.   | Et (p, q) -> (évalue_dans liaisons p) &  (évalue_dans liaisons q)
  6.   | Ou (p, q) -> (évalue_dans liaisons p) or (évalue_dans liaisons q)
  7.   | Implique (p, q) ->
  8.       (not (évalue_dans liaisons p)) or (évalue_dans liaisons q)
  9.   | Équivalent (p, q) ->
  10.       évalue_dans liaisons p = évalue_dans liaisons q
  11.   | Variable v -> assoc v liaisons;;
  12. let rec vérifie_lignes proposition liaisons variables =
  13.   match variables with
  14.     [] ->
  15.      if not évalue_dans liaisons proposition
  16.      then raise (Réfutation liaisons)
  17.   | var :: autres ->
  18.      vérifie_lignes proposition ((var, true) :: liaisons) autres;
  19.      vérifie_lignes proposition ((var, false):: liaisons) autres;;
  20.  
  21. let vérifie_tautologie proposition variables =
  22.   vérifie_lignes proposition [] variables;;
  23. let rec variables accu proposition =
  24.   match proposition with
  25.     Variable v -> if mem v accu then accu else v::accu
  26.   | Non p -> variables accu p
  27.   | Et (p, q) -> variables (variables accu p) q
  28.   | Ou (p, q) -> variables (variables accu p) q
  29.   | Implique (p, q) -> variables (variables accu p) q
  30.   | Équivalent (p, q) -> variables (variables accu p) q
  31.   | _ -> accu;;
  32.  
  33. let variables_libres proposition = variables [] proposition;;
  34.